Review fixes for prove-and-retire (#994) - #995
Merged
Merged
Conversation
`verify_batched`'s fold seed indexes both out-of-domain blocks at the `width`/`height` the proof advertises, but `ood_blocks_well_formed` — the guard that pins those dimensions to the AIR and calls `dimensions_consistent()` — did not run until 92 lines later. A proof whose advertised dimensions disagree with its data length therefore panicked in `Table::get_row`'s unchecked slice rather than being rejected. That is the exact gap the guard's own doc comment says it exists to close, and the ordinary verifier keeps the ordering by running it inside the round-1 loop. Hoist the three shape checks into the pre-pass that already validates each table's domain, before any of them is read. The division by `trace_length` is safe there: the same loop rejects zero first. No transcript byte moves — the checks touch no transcript. `prover::batched_verifier::replay` had the same pre-guard read through `Table::columns`; it is test-only, but a patch that fixed only the STARK half would leave a reader thinking the family was covered. Direction is robustness, not soundness: nothing wrong is accepted, the verifier aborts instead of returning false. It is unreachable from bytes today because `BatchedProof` has no derives — which is also why it is the cheapest moment to pay for it, since serializing that format is the point. Also drop `Replay::iotas`, documented as the per-group query indices and always empty, and say plainly that `replay` is a test oracle: it takes the prover's word on the precomputed root and never checks `fold_order` is a permutation, both of which `verify` does. `a_tampered_batched_proof_is_rejected` grows five arms: a group's FRI layer root (the one commitment batching relocated from per-table to per-group), a main root, a composition root, an out-of-domain value, and a block whose advertised width lies. The last one panics at `table.rs:362` without this change and is rejected with it.
Each of these inserted a new item between an existing doc comment and the
item it documented, with no blank line, so rustdoc merged the two blocks and
the original item lost its docs:
prover.rs table_parallelism -> MainRoots
prover.rs plain -> known_roots
verifier.rs replay_rounds_* -> replay_rounds_2_and_3
decode.rs update_multiplicities -> add_multiplicities
trace_builder.rs cpu32_chip_op -> WalkLeftover
trace_builder.rs build_initial_image-> runtime_page_ranges
trace_builder.rs touched_memory_cells -> op_count
trace_builder.rs collect_epoch -> walk_and_emit_chunks
Three of the adopted sentences were actively wrong about their new owner:
`known_roots` was labelled "for a plain (non-preprocessed) table" when it
takes `precomputed: Option<Commitment>` and serves both; `add_multiplicities`
was described in terms of a `lookups` parameter it does not have; and
`WalkLeftover`'s public rustdoc opened by describing an ALU dispatch helper.
`replay_rounds_2_and_3` is renamed `replay_rounds_2_to_4`: its body still
carries an explicit `Round 4` section sampling gamma and the DEEP
coefficients, so the orphaned sentence ("rounds 2, 3 and 4") was the accurate
one and the new name was not.
`bitwise_histogram` carried two stacked doc blocks, the first saying LT, MUL,
DVRM, SHIFT, the accelerators and PAGE "are not here yet" and the second,
directly below, saying the histogram is complete. The first is left over from
an earlier state; `finalize` folds all of them in.
Two claims about residency were wrong in the same way. `pass.rs`'s header said
what the walk holds is one table plus the residents "no matter how long the run
is", and the design doc listed LT among the tables handed over "as soon as a
chunk fills". LT is not: it, MUL, DVRM and SHIFT are deliberately absent from
`CHUNKED_KINDS` because later derivations keep appending to them, so their
chunk boundaries are not knowable until the run ends — `walk_and_emit_chunks`'s
own doc comment says so two paragraphs below the sentence that contradicted it.
Their op lists, the `retired_*` rows a closing chunk converts its ops into, and
the walk's BITWISE lookups are all held whole, so that term is O(cycles).
It is a small term — compact routed intermediates against trace rows, a low
single-digit percentage of the measured peak — and closing it would move LT's
chunk boundaries and cost the byte-identical-roots property that makes the
per-table variant a drop-in. So this changes no code: it makes the documents
say what the code does, and lists the gap in §10 with the observation that
BITWISE's half is the cheap one, since a histogram is commutative and could be
folded per segment without moving any root.
Also in the design doc:
- the `A1_TABLE_PARALLELISM` row quoted a sweep ("flat between 12 and 24; 24
costs 6 GB") that does not match the one recorded on `pass::table_parallelism`
(no k=12 or k=24 rows; the step is 16 -> 32 for 5.0 GB);
- `A1_INFLIGHT` and `LAMBDA_STREAM_LDE` were missing from a table that claims to
list every knob, and the second changes this approach's own memory profile;
- `--features hash-metrics` is from #987, which is not on this branch, so the
verify-hash column cannot be reproduced here — say so rather than give a
build command that fails;
- "the spec's Open optimization ... was not kept" described code that ships:
what was dropped is holding whole Merkle trees between passes, while
leaf-dropping is `drop_leaves`/`retire_leaves` behind `LAMBDA_STREAM_LDE`;
- §6's header omitted the blowup and the knob settings the numbers were taken
at.
And five comments said the ethrex block has 227 tables where the doc says 245.
Rather than guess which run is stale, they now say "once per table" and the
like: none of them needed the number.
Three things, all outside the prove-and-retire path. `keep_large_buffers_warm()` ran as the first statement of `main()`, so every subcommand — `prove`, `verify`, `execute`, `--help` — allocated 16 MiB, disabled dirty decay on the oversize arena for the life of the process, and left a 10-second purge thread behind. Disabling decay retains RSS that `auto_storage::available_ram_bytes()` does not model, and it is the sort of change that quietly moves every memory number taken with this binary. Call it from the prove-and-retire path, which is the one that allocates and drops trace-sized buffers in a loop. Both of its mallctl failure paths returned silently, and `env_logger::init()` ran on the next line, so nothing could have been logged even if it had tried. A run where the knob did not land was indistinguishable from one where it did. They now warn. The doc comment also records why `opt.narenas` is the right index — jemalloc 5 reserves the slot after the automatic arenas for the oversize arena (`arena_init_huge`), whose threshold defaults to the same 8 MiB the comment names — since a count used as an index invites a second look. `tikv-jemalloc-ctl` had become a hard dependency carrying `features = ["stats"]`, and `jemalloc-stats` an empty feature. That propagates to `tikv-jemalloc-sys/stats` and so to `--enable-stats`, which puts counters on the malloc fast path of every CLI build, including ones measuring baselines. `keep_large_buffers_warm` needs only `raw`/`mallctl`, so the dependency stays and `stats` goes back behind `jemalloc-stats`, which is what the heap tracker is gated on anyway. Finally, `--output` with any stage but `logup` walked the whole execution, returned no proof, wrote no file and exited 0 — and with `--through batched` it also forced a verification the user had not asked for, because `--output` is OR'd into the `verify` argument. It now fails before the walk with a message naming the stage.
`retire_lde_proof_is_byte_identical` compared a proof against itself under
`cuda`: there `retire_leaves` returns `None` unconditionally and
`retire_main_lde` is compiled out, so both arms take the resident path. That
configuration is not hypothetical — `make test-prover-cuda` runs this suite on
the merge queue. It is now `#[cfg(not(feature = "cuda"))]`, and each arm
asserts `streaming_retire_lde()` actually returned what it set, so the test
fails rather than passes if the flag ever stops taking effect.
Its `ENV_LOCK` was a function-local `static` that nothing else could name, and
libtest calls each `#[test]` once, so it could never be contended — it guarded
nothing, and the SAFETY comment above the `set_var` ("single-threaded section
guarded by ENV_LOCK") was false on both clauses. Replaced with what is actually
true: this is the only writer in the binary, every reader goes through
`std::env`, which serialises readers against writers on its own lock, so the
exposure is other tests observing the flag under a plain `cargo test` — their
coverage, not memory safety. `cargo nextest`, which CI runs, forks per test.
The note names the real fix (its own integration binary, as
`prover/tests/gpu_force_downgrade.rs` already does) without doing it here.
`checkpoint_tests`' `assert!(full.len() > 100_000)` followed an
`assert_eq!(full.len(), N_ADDI + 1)` with `N_ADDI = 100_005` — a tautology. The
property it was reaching for is already checked by the `logs.len() <
full.len()` assertion further down.
`chunk_shape_matches_the_built_chunk` gave ops to LT only, so for the other
thirteen kinds both sides collapsed to the 4-row padding floor and only the
column width was pinned. The row half was covered, but by one kind — so a
divergence in a single generator's padding would be missed. It now also
populates MUL (dedup, like LT) and SHIFT (plain, 20 ops over a limit of 8, so
its chunks are 8/8/4 and sit above the floor), asserts each fixture exercises
what it is there for, and counts populated chunks so the loop cannot silently
go back to comparing constants.
`prover/src/tests/mod.rs` declared `batched_fri_tests` and
`challenge_phase_tests` without the `#[cfg(test)]` every other entry carries;
the parent `mod tests` is ungated, so those two were the only ones compiled
into a non-test build of the library.
`cargo fmt --all`, plus a `clone()` on a `Copy` field that the new out-of-domain tamper arm introduced.
`keep_large_buffers_warm`'s warnings are inside `#[cfg(target_os = "linux")]`, so a macOS build never compiles them and my local lint runs said nothing. CI, on Linux, did: `use of unresolved module or unlinked crate log`. `log` was reaching `bin/cli` only as a transitive dependency of `env_logger`, which is not a dependency you may name. Declared, with a note on the file that its only user is Linux-gated.
`make compile-recursion-elfs` compiles `lambda-vm-prover` for the RISC-V guest, where `parallel` is off and there is no rayon. The three new phase modules `use rayon::prelude::*` unconditionally and call `into_par_iter`/`par_iter`, so the recursion guest stopped building: 27 errors, 8 unresolved-`rayon` and 9 missing-method, plus three `E0505`s in `trace_builder`. This is on #994's branch as it stands, not introduced by this PR — the same `cargo check -p lambda-vm-prover --no-default-features` fails identically at `f800e4b0`. It went unnoticed because no CI run has ever touched that branch; this PR is the first, which is how it surfaced. The four `make lint` arms do not catch it either: the workspace-level `--no-default-features` arm still resolves `parallel` through another member's feature unification. Gated with the idiom already used in `trace_builder.rs` — a `#[cfg]` pair around the iterator source, serial arm `into_iter`/`iter`. Where the closure was long enough that duplicating it would be worse than the problem, it is hoisted to a named binding first and both arms map over that, so the body appears once. No behaviour change on any path that runs today: the serial arms exist to compile for the guest, which links the crate for its verifier and never executes these phases. The `E0505`s were the serial arm of the BITWISE collector loop iterating `&collectors` where the parallel arm moves it into `units`, so the closures' borrows of the op lists outlived the point where `CollectedOps` moves those lists. Consumed by value, matching the parallel arm. Verified: `make compile-recursion-elfs` succeeds, all four `make lint` arms and `cargo fmt --check` pass, and the prove-and-retire tests are unchanged at 13/13.
jotabulacios
added a commit
that referenced
this pull request
Sep 20, 2026
Brings in origin/perf/streaming-retire-lde (#995): the review corrections over the prove-and-retire work, not new functionality. The batched verifier now validates the declared block dimensions against the AIR before reading the out-of-domain blocks, so a proof with dishonest dimensions is rejected instead of panicking the verifier. tikv-jemalloc-ctl moves behind a feature so its stats counters stay out of the malloc fast path of every CLI binary, and the warm-buffer preallocation runs only in the subcommand that needs it; both were skewing the baselines we measure against. The CLI now errors on --output for stages other than logup instead of walking the whole run and exiting 0 without writing anything. Four tests that could not fail are fixed, including one that compared a proof against itself under cuda. Three resolutions. In prover/src/tests/mod.rs the incoming #[cfg(test)] gating wins: it keeps those test modules out of non-test builds of the library, which is the problem it was written for, while the parallel gate it replaces addressed something else and is now obsolete. In logup_phase.rs our move of BatchedProof to batched_proof.rs wins, since the type has to be reachable when the parallel feature is off; the definitions are otherwise identical field by field, and logup_phase re-exports it so existing paths keep working. In tables/trace_builder.rs git merged both sides cleanly and produced code that does not compile: both branches fixed the same borrow of the collector list, one by consuming it in the loop and one by dropping it afterwards, leaving a use of a moved value in builds without parallel. The drop is removed and the by-value loop stays.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fixes from an adversarial review of #994, onto its own branch so the review
trail stays separate from the feature work. Six commits, +370/−131, no
behaviour change to the proving path.
The one that matters
verify_batched's fold seed indexed both out-of-domain blocks at thewidth/heightthe proof advertises, 92 lines beforeood_blocks_well_formedpinned those dimensions to the AIR. A proof whoseadvertised dimensions disagree with its data length panicked in
Table::get_row's unchecked slice instead of being rejected. The guard's owndoc comment says it exists to close exactly that, and the ordinary verifier
keeps the ordering by running it inside the round-1 loop.
The three shape checks now run in the pre-pass that already validates each
table's domain. No transcript byte moves — the checks touch no transcript.
prover::batched_verifier::replayhad the same pre-guard read viaTable::columnsand gets the same treatment.Direction is robustness, not soundness: nothing wrong was accepted, the
verifier aborted instead of returning
false. It is unreachable from bytestoday because
BatchedProofhas no derives — which is also the cheapest momentto pay for it, since serializing that format is the point of the format.
a_tampered_batched_proof_is_rejectedgains five arms, including one thatlies about a block's width. That arm panics at
crypto/stark/src/table.rs:362without this change and is rejected with it — checked both ways.
The rest
keep_large_buffers_warm()ran as the first statement ofmain(), soverify,executeand--helpall disabled dirty decay on the oversizearena for the process lifetime and left a purge thread behind. It now runs
only on the prove-and-retire path, and its two silent
returns log.Separately,
tikv-jemalloc-ctlhad become non-optional withfeatures = ["stats"], which propagates to--enable-statsand put jemalloccounters on the malloc fast path of every CLI build — including ones
measuring baselines.
statsgoes back behindjemalloc-stats.--outputwith any stage butlogupwalked the whole execution, wrotenothing and exited 0 (and with
--through batchedalso forced averification, since
--outputis OR'd intoverify). It now fails beforethe walk.
retire_lde_proof_is_byte_identicalcompared a proof to itself under
cuda(a live merge-queue config) and nowskips there and asserts the flag took effect; a
> 100_000tautology incheckpoint_tests; andchunk_shape_matches_the_built_chunkcovered the rowhalf for LT only, so a single generator's padding change would slip through —
it now populates MUL and SHIFT too, the latter above the 4-row padding floor.
what they documented; three of the adopted sentences were wrong about their
new owner.
replay_rounds_2_and_3is renamedreplay_rounds_2_to_4becauseits body still has a
Round 4section.pass.rssaid the walk holds one table plusthe residents "no matter how long the run is", and the design doc listed LT
among the tables handed over as a chunk fills. LT, MUL, DVRM and SHIFT are
deliberately excluded from
CHUNKED_KINDS— later derivations keep appendingto them — so their op lists are held whole and that term is O(cycles). It is
a small term and closing it would move LT's chunk boundaries and cost the
byte-identical-roots property, so no code changed: the documents now say
what the code does, and §10 records the gap.
in
pass.rs;A1_INFLIGHTandLAMBDA_STREAM_LDEmissing from a table thatclaims to list every knob; a
--features hash-metricsbuild command thatcannot work here (tooling(recursion): count keccak hashes to verify a proof (excl. grin… #987 is not on this branch, so the verify-hash column is not
reproducible); "the spec's Open optimization was not kept" describing code
that ships behind
LAMBDA_STREAM_LDE; and §6's header missing the blowup andknob settings.
TableDeep::air_index(alwaysusize::MAX, never read, with adoc describing a mechanism that does not exist),
Replay::iotas(documentedas the query indices, always empty), and a
group_ofloop that linearlysearched the list it was iterating for the element it already held, ending in
an unreachable
expecton the prover path.get_proof_by_pos_with_leaf_siblingreadself.nodesdirectly where everyother read in that file goes through
node_get's disk-spill indirection.Unreachable today, but the prover's opening path
expects the result.Verification
make lint's four clippy arms (including--features lambda-vm-prover/cudawith stub cubins) and
cargo fmt --all --checkall pass. Tests run in release:all 8
batched_fri_tests, all 4challenge_phase_tests,chunk_shape_matches_the_built_chunk, both newmerkle_tests,prove_verify_roundtrip_testsandcheckpoint_tests— green.Not verified here: anything needing a GPU, and the ethrex block itself. The
numbers in the design doc are untouched and still rest on the author's runs.
Deliberately not addressed
AIRs optional and moved them after HALT, so the fixed prefix is no longer a
constant. Six sites break loudly;
prover/src/streaming.rs'sNUM_FIXED_AIRS = 10, feedingAirOrder::first_chunked(), auto-merges cleanand is silently wrong on any program without ECSM and HINT rows — which is
every fixture here. That is a design decision plus a re-measurement, not a
review fix.
challenge_phase.rsand threesites in
logup_phase.rs), where array position is the transcript-forkindex and only the length is compiler-checked. Worth collapsing to one shared
accessor — but the Feat/skip empty tables #977 resolution has to touch all four anyway, so doing it
here would only conflict.
gap (a histogram is commutative, so no root moves). It is a perf change and
belongs with a measurement on the boxes.